package metro.sato;

import metro.sato.EscribeFichero;

/**
 * Clase para la generacion de clausulas admitidas por SATO para la resolucion
 * de un problema con n trenes y m estaciones
 * 
 * @author finrox
 */
public class GeneraClausula {

	private final Integer t;
	private final Integer e;
	private String f;
	private boolean eo;
	private static final String pT = "1";

	/**
	 * Constructor de la clase
	 * 
	 * @param trenes
	 *            nuemro de trenes en el metro
	 * @param estaciones
	 *            numero de estaciones en el metro
	 * @param ficheroSalida
	 *            fichero para SATO
	 * @param estacion
	 *            ocupada incluyo condicion de estacion ocupada
	 */
	public GeneraClausula(Integer trenes, Integer estaciones,
			String ficheroSalida, boolean estacionOcupada) {

		t = trenes;
		e = estaciones;
		f = ficheroSalida;
		eo = estacionOcupada;

	}

	/**
	 * Genero las clausulas SATO para el problema y las escribo en el fichero de
	 * salida especificado
	 */
	public void genera() {

		EscribeFichero eF = new EscribeFichero(f);
		eF.pantalla = true;

		// el tren tiene que estar en alguna de las estaciones o en transito
		// hacia alguna de ellas
		eF.escribeln("#Posibilidades");
		for (Integer i = 1; i <= t; i++) {
			for (Integer j = 1; j <= e; j++) {
				eF.escribe(i.toString() + j.toString() + " " + pT
						+ i.toString() + j.toString() + " ");
			}
			eF.escribeln("");
		}

		// si el tren esta en una estacion otro tren no puede estar en esa misma
		// estacion
		eF.escribeln("");
		eF.escribeln("#En una estacion solo cabe un tren");
		for (Integer i = 1; i <= e; i++) {
			for (Integer j = 1; j < t; j++) {
				for (Integer k = j + 1; k <= t; k++) {
					eF.escribeln("(-" + j.toString() + i.toString() + " -"
							+ k.toString() + i.toString() + ")");
				}
			}
		}

		// si el tren esta en una estacion ese mismo tren no puede estar en otra
		// estacion
		eF.escribeln("");
		eF.escribeln("#Un tren solo puede estar en una estacion");
		for (Integer i = 1; i <= t; i++) {
			for (Integer j = 1; j < e; j++) {
				for (Integer k = j + 1; k <= e; k++) {
					eF.escribeln("(-" + i.toString() + j.toString() + " -"
							+ i.toString() + k.toString() + ")");
				}
			}
		}

		// si el tren esta en transito hacia una estacion otro tren no puede
		// estar en transito hacia esa misma estacion
		eF.escribeln("");
		eF.escribeln("#En una via solo cabe un tren");
		for (Integer i = 1; i <= e; i++) {
			for (Integer j = 1; j < t; j++) {
				for (Integer k = j + 1; k <= t; k++) {
					eF.escribeln("(-" + pT + j.toString() + i.toString() + " -"
							+ pT + k.toString() + i.toString() + ")");
				}
			}
		}

		// si el tren esta en transito hacia una estaccion no puede estar en
		// transito hacia otra estacion
		eF.escribeln("");
		eF.escribeln("#Un tren solo puede ir en un sentido");
		for (Integer i = 1; i <= t; i++) {
			for (Integer j = 1; j < e; j++) {
				for (Integer k = j + 1; k <= e; k++) {
					eF.escribeln("(-" + pT + i.toString() + j.toString() + " -"
							+ pT + i.toString() + k.toString() + ")");
				}
			}
		}

		// si el tren esta en una estacion no puede estar en transito hacia una
		// estacion
		eF.escribeln("");
		eF.escribeln("#Si esta en estacion no esta en transito");
		for (Integer i = 1; i <= t; i++) {
			for (Integer j = 1; j <= e; j++) {
				for (Integer k = 1; k <= e; k++) {
					eF.escribeln("(-" + i.toString() + j.toString() + " -" + pT
							+ i.toString() + k.toString() + ")");
				}
			}
		}

		if (eo) {
			// si el tren esta en transito hacia una estacion esa estacion no
			// puede estar ocupada por otro tren
			eF.escribeln("");
			eF.escribeln("#Estacion ocupada por otro tren");
			for (Integer i = 1; i <= e; i++) {
				for (Integer j = 1; j <= t; j++) {
					for (Integer k = 1; k <= t; k++) {
						if (j != k)
							eF.escribeln("(-" + pT + j.toString()
									+ i.toString() + " -" + k.toString()
									+ i.toString() + ")");
					}
				}
			}
		}

		eF.cierra();
	}

}
